The present invention relates to testing computer software programs and, more particularly, to a technique for testing event driven application programs.
In well-known event driven software systems (also referred to in the art as xe2x80x9creactive systemsxe2x80x9d), certain functionality occurs when an event is generated and communicated to an executing process performing particular actions based upon the occurrence of the particular event. More particularly, event driven software is used to define the behavior of a system, e.g., a computer, in response to events that are generated by other systems, machines or peripheral devices connected thereto. Well-known examples of event driven systems include: telecommunications applications, call-processing software, data communications software, device drivers, and computer interface applications. As will be appreciated, these types of event driven systems are state oriented. That is, in each state of a system, one specific event from a predefined set of events is expected to occur, and the system is designed to respond to the event in a well-defined manner.
Briefly, as is well-known, a state machine converts a time series of event stimuli or input data through some function into a time series of responses or output data. For example, in an event driven system, at each point in time, each machine is in a particular so-called xe2x80x9ccontrol statexe2x80x9d which defines the events that are expected to be generated by other machines, and the type of responses that are to be generated upon the arrival of each such event. Typically, the response includes the execution of a finite piece of program code, the generation of new events, and the identification of a new control state for the particular machine responding to the incoming events. Thus, the state machine model of the event driven system plays a critical role in the development of the application program code by the programmer for the system.
Typically event driven application software is written in higher level general-purpose programming languages such as the well-known xe2x80x9cCxe2x80x9d or xe2x80x9cC++xe2x80x9d programming languages, or a special-purpose language such as the well-known ITU Systems Description Language (xe2x80x9cSDLxe2x80x9d). In developing the actual program code for such systems it is common to describe the behavior of the relevant machines in terms of state machines. Using a higher level programming language, e.g., C, software programmers will write event driven software code for the particular application. Typically, the software program development begins by reviewing a so-called system specification which provides a logical description of the desired operations for the application. Working from the specification, one or more programmers will write the necessary code to implement the operations.
This conventional programming process results in an application program which contains no particular visual context amongst and between the various control states of the event driven system. That is, the program code can be viewed as one large xe2x80x9cflatxe2x80x9d file with a series of program instructions. Further, as the original specification changes during program development, e.g., additional functionality is added to the system, the requisite program code and additional control states are typically added to the source program in a somewhat arbitrary order. In order for a programmer to understand the logical flow from control state-to-control state directly from the program source code it is necessary to manually trace the execution thread through the source, e.g., tracing branch instructions or xe2x80x9cgotoxe2x80x9d statements. As will appreciated, the tracing of such logical flow, particularly in very large source code programs, is a tedious and time consuming task. This also leads to certain complexity in the testing of the software for so-called xe2x80x9cbugsxe2x80x9d and to determine whether the application program implements the desired features.
More particularly, a critical state in the development of the application software code for such systems is the testing of the code to validate the properties of the software and to insure that the behavior of the system complies with the design objectives. There are a number of well-known methods for testing event driven software. For example, Boris Beizer, Black-Box Testing: Techniques for Functional Testing of Software and Systems, John Wiley and Sons, 1984, describes a well-known testing arrangement wherein a set of test goals is defined from which a limited set of test sequences is deduced. Typically, the set of test sequences is defined through a manual process by the testing engineer through examination of the system design. The set of test sequences is applied to the event driven software under test and either a xe2x80x9cpassxe2x80x9d or xe2x80x9cfailxe2x80x9d is recorded as the testing result. This testing methodology is typically applied to general software testing and is well-known in the art to be prone to human error and incomplete. In particular, the number of possible executions of the event driven software under test is incredibly large. In contrast, the number of tests that can be performed on the software with real-time executions is limited by certain practical constraints such as the minimum time required to perform a single test from the total number of tests. As such, it is typical that no more than a few hundred tests can be selected and applied in accordance with this methodology. This results in a very low confidence level in the testing coverage.
A second event driven software method known in the art is described, e.g., by D. Lee et al, Principles and Methods of Testing Finite State Machinesxe2x80x94A Survey, Proceedings of the IEEE, Vol. 84, pp. 1090-1126, 1996. In accordance with this testing method, an abstract state machine model for the event drive software program is constructed. The state machine model typically captures only a high-level description of the program code thereby leaving out most of the program details. Thereafter, well-known test sequence generation algorithms (see, e.g., Lee, supra.) can be applied to the state machine model from which a relatively small set of tests is derived and applied to the software under test. As with the above-described testing method, this technique relies heavily on the manual construction of the abstract model of the event driven software. Therefore, this technique is sensitive to certain errors caused by mismatches between the formal relation between the software under test and the abstract model to be used for deriving the applicable tests. In addition, changes to the event driven software require the development of new tests which proves cumbersome and time consuming.
In a third commonly used testing method, see, e.g., C. H. West, Protocol Validation by Random State Exploration, Proc. 6th IFIPWG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification, North-Holland Publ., pp. 233-242, 1986, a random exploration of the full behavior of the event driven software is undertaken in order to establish the software""s compliance with the desired properties. The amount of detail in the full software description generally precludes any attempt to perform an exhaustive exploration of the software for testing purposes. Therefore, well-known statistical algorithms are used to extract and analyze random samples of the software""s behavior. However, as with the other above-described testing arrangements, one recognized drawback in this testing approach is that the amount of extraneous detail in the full software description prevents an efficient exhaustive exploration of the full behavior of the software for compliance with high-level properties.
Therefore, a need exists for a technique that mitigates the above-described problems in the art and improves the programming development and testing of event driven software.
The present invention provides a technique for testing event driven software directed to the efficient testing of event driven software and making it possible to track the validity of future changes to the program code, as part of the normal maintenance, extension and revision process to the source code. More particularly, in accordance with the preferred embodiment of the invention, event driven software code is specified and written in accordance with the principles of the co-pending, commonly assigned patent application, entitled xe2x80x9cMethod and Apparatus For Developing Event Driven Softwarexe2x80x9d, application Ser. No. 09/212,069, filed on event date herewith. That is, in accordance with the preferred embodiment, the source code program is defined and structured into control-sensitive and non-control-sensitive format. In accordance with the present invention, the event driven source code program is parsed to extract the control states defined in the source program, and to convert the source code into an intermediate state machine format. Thereafter, in accordance with the invention, the intermediate state machine format is converted into a automata-based format for modeling checking purposes.
In particular, in accordance with the preferred embodiment, the intermediate state machine format is converted into an annotated automaton model. Illustratively, the annotated automaton model is a verification program written in the input language of a specific model checker. Importantly, in accordance with the invention, each statement from the source code program is mapped onto an abstraction within the automaton model. The mapping is achieved using a translation map which is defined at the initial stage of the verification process. The map need not be revised thereafter unless new types of instructions are introduced, e.g., after revisions are made to repair programming faults, into the source program. The mapping, inter alia, dictates a fixed translation of the particular statement into the target language of the model checker. Thus, instructions that appear in the map are systematically converted into the automaton model wherever such instructions appear in the source code.
In addition to the above-described map, in accordance with the invention, a so-called environment model is defined which encapsulates a minimal set of assumptions that must be made about the particular operating environment in which the event driven application is executed. More particularly, as the model checker input language is provided to the model checker, the environmental model is applied. As a result, in accordance with the preferred embodiment of the invention, the verification of the properties of the event driven system is made subject to the environmental model during the testing and checking of the event driven software by the verification system. Thereafter, the testing and checking results are output, in a well-known manner, by the model checker for determining whether the event driven system conforms with the user""s desired execution properties and behaviors.
Advantageously, in accordance with the invention, the model extraction process and application of the model checker occurs in a direct and dynamic fashion from the event driven system program code without the need for user intervention.